#ifndef PRINCESSFORMULAPARSER_H_
#define PRINCESSFORMULAPARSER_H_
#include <sstream>
#include <map>
#include <cmath>
#include <stack>
#include <set>
using namespace std;
#include "typedef.h"

class PrincessFormulaParser {

public:
  PrincessFormulaParser(const string& charSeq)
    : charSeq(charSeq), currentPos(0),
      hasNextToken(false), nextToken("") {
    computeNextToken();
  }

  Prop* parse() { return parseFormula(1); }

private:

  typedef set<Expr*> Quans;
  typedef stack<Quans> QuanStack;
  QuanStack quanStack;

  const string charSeq;
  unsigned int currentPos;
  istringstream tokens;
  bool hasNextToken;
  string nextToken;

  Prop* parseFormula(int polarity);
  Expr* parseTerm(bool& untranslatable);
  void expect(const string& token);
  void consumeWhiteSpaces();
  void computeNextToken();

};
#endif
